/*
 * To change this template, choose Tools | Templates
 * and open the template in the editor.
 */
package chameleon.model.NuGatStructure.strategy;

import chameleon.model.NuGatStructure.game.GamePlayer;
import chameleon.model.NuGatStructure.prop.PropGame;
import chameleon.model.NuGatStructure.utils.Node;
import chameleon.model.NuGatStructure.fsm.GameBddFsm;
import chameleon.model.NuGatStructure.bdd.Bdd;
import chameleon.model.NuGatStructure.enc.BddEnc;
import chameleon.gameSolver.NuGat.NuGatInterface;
import chameleon.model.NuGatManager.Strategy.PreImage;
import chameleon.model.NuGatManager.Strategy.PreImageComputation;
import chameleon.model.NuGatStructure.fsm.BddFsm;
import chameleon.model.game.Game;
import chameleon.view.OutputManager;
import com.sun.jna.Pointer;

/**
 *
 * @author simon
 */
public class ReachAvoidStrategy extends GameStrategy {
    
    private PreImage preImage_;
    
    //********************* CONSTRUCTOR *************************************//
    
    public ReachAvoidStrategy(GameBddFsm fsm,
            GamePlayer player,
            int reverseInitialQuantifiers,
            Bdd goal,
            Bdd winningStates,
            Bdd trans,
            PreImage preImage,
            PropGame prop,
            NuGatInterface nugat){
        super(nugat.GameStrategy_construct(fsm.ptr(),
                player.ptr(),
                reverseInitialQuantifiers,
                goal.ptr(),
                winningStates.ptr(),
                trans.ptr()),nugat);
        preImage_ = preImage;
        reverseInitialQuantifiers_ = reverseInitialQuantifiers;
        prop_ = preImage.getProp();
    }
    
    private ReachAvoidStrategy (BddEnc bdd_enc,
                     GamePlayer player,
                     int reverseInitialQuantifiers,
                     Bdd init_goal,
                     Bdd init_opponent_deadlock,
                     Bdd init_moves,
                     Bdd goal,
                     Bdd opponent_deadlock,
                     Bdd moves,
                     PropGame prop,
                     NuGatInterface nugat){
        super(nugat.GameStrategy_create(bdd_enc.ptr(),
                player.ptr(),
                reverseInitialQuantifiers,
                init_goal.ptr(),
                init_opponent_deadlock.ptr(),
                init_moves.ptr(),
                goal.ptr(),
                opponent_deadlock.ptr(),
                moves.ptr()),prop, nugat);
    }
    
    @Override
    public final ReachAvoidStrategy clone(){
        ReachAvoidStrategy strategy =  new ReachAvoidStrategy(this.getBddEnc(),
                this.getPlayer(),
                this.getReverseInitialQuantifiers(),
                this.getInitGoal(),
                this.getInitOpponentDeadlock(),
                this.getInitMoves(),
                this.getGoal(),
                this.getOpponentDeadlock(),
                this.getMoves(),prop_, nugat_
                );
     strategy.setPreImage(this.preImage_);
     strategy.setReverseInitialQuantifiers(reverseInitialQuantifiers_);
     return strategy;
    }

    //*********************** DESTRUCTOR ************************************//
    
    @Override
    public void destroy(){
        preImage_.destroy(getBddEnc().getDdManager());
        super.destroy();
    }
    
    //*********************** PRINT ****************************************//
    /**
     * Print the strategy in the given file.      * 
     * @param file 
     */
    @Override
    public final void printStrategy (String file){
        checkStrategyExistence();
        ReachAvoidStrategy strategy = this.clone();
        printStatus();
        
        nugat_.Chameleon_Game_AfterCheckingSpec(preImage_.getProp().ptr(),
                     preImage_.getStatus(),
                     strategy.ptr(),
                     Pointer.NULL, 
                     Pointer.NULL,
                     1,0, 1, file);
        
    }
    
    @Override
    public final void printStatus(){
        super.printStatus();
        OutputManager output = new OutputManager();
        switch (preImage_.getStatus()) {
            case NuGatInterface.GAME_REALIZABLE:
                output.displayString(" : the strategy has been found\n");
                break;
            case NuGatInterface.GAME_UNREALIZABLE:
                output.displayString(" : no strategy exists\n");
                break;
            case NuGatInterface.GAME_UNKNOWN:
                /* status should remain unknown */
                output.displayString(" : existence of a strategy is unknown\n");
                break;
            default: throw new RuntimeException("unknown status of a problem");
        }
        
    }

    //************************ SETTER **************************************//
    
    public final void setPreImage(PreImage preImage_) {
        this.preImage_ = preImage_;
    }

    //************************ GETTER *************************************//
    
    @Override
    public Node getLtlSpec() {
        throw new UnsupportedOperationException("Not supported yet.");
    }

    
    /**
     * This method check if the strategy present at the moment is winning. 
     * This strategy can be different than the original strategy provide by NuGaT.
     * Typically this strategy is a subset of the initial strategy. 
     * 
     * 
     * This checking is done by replay the game by fixing one player. This player
     * play the strategy.
     * @param game 
     */
    
    /*@Override
    public void strategyIsWinning(Game game){
        GameBddFsm originalFsm = game.getGameBddFsm();
        GameBddFsm fsm ;
        
        GamePlayer player = getPlayer();
        String strPlayer = player.toString();
        
        BddFsm playerBddFsm;
        BddFsm stratBddFsm;
        
        if (strPlayer.equals(nugat_.PLAYER_NAME_1)){
            playerBddFsm = game.getBddFsmP1().clone();
        }
        else{
            playerBddFsm = game.getBddFsmP2().clone();
        }
        
        
        //create the strategy bdd fsm
        stratBddFsm = getBddFsm(playerBddFsm, game.getOptsHandlerInstance(),
                game.getGlobalFsmBuilder());
        
        //Replace the transition relation for the player in the game fsm
        if (strPlayer.equals(nugat_.PLAYER_NAME_1))
            fsm = originalFsm.changePLayer1(stratBddFsm);
        else
            fsm = originalFsm.changePLayer2(stratBddFsm);
        
        PreImageComputation computation = new PreImageComputation(nugat_, prop_);
        PreImage preImage = computation.compute(enc_, game.getOptsHandlerInstance(), fsm);
        
        OutputManager output = new OutputManager();
        if (preImage.getStatus()==nugat_.GAME_REALIZABLE)
            output.displayString("The strategy is winning\n");
        else
            output.displayString("The strategy is not winning\n");
        
    }*/
}
